Nuprl Lemma : d-feasible-dec
0,22
postcript
pdf
D
:Dsys.
Feasible(
D
)
j
,
b
:Id
s
:M(
j
).state
Dec(
b
in dom(M(
j
).pre) & (
v
:M(
j
).da(locl(
b
)). M(
j
).pre(
b
,
s
,
v
)))
latex
Definitions
x
:
A
.
B
(
x
)
,
P
Q
,
t
T
,
Feasible(
D
)
,
P
&
Q
,
Prop
Lemmas
ma-st
wf
,
d-m
wf
,
Id
wf
,
d-feasible
wf
,
dsys
wf
origin
D:Dsys.
j,b:Id
s:M(j).stateDec(b in dom(M(j).pre) & (
v:M(j).da(locl(b)). M(j).pre(b,s,v))) D:Dsys.
j,b:Ids:M(j).stateDec(b in dom(M(j).pre) & (v:M(j).da(locl(b)). M(j).pre(b,s,v))) x:A. B(x) Q
T